The following papers provide useful background information, for which they are incorporated herein by reference in their entirety, and are selectively referred to in the remainder of this disclosure by their accompanying reference numbers in square brackets (i.e., [4] for the fourth paper, by R. E. Bryant).    [1] R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. 5th Symp. On Logic in Computer Science (LICS 90), pages 414-425, 1990.    [2] C. W. Barrett, D. L. Dill, and A. Stump. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. LNCS, 2404:236-249, 2002.    [3] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zh. Symbolic model checking without BDDs. LNCS, 1579, 1999.    [4] R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, August 1986.    [5] R. E. Bryant, S. German, and M. N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. LNCS, 1633:470-482, 1999.    [6] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. LNCS, 1855:154-169, 2000.
[7] E. M. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7-34, 2001.
[8] F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella, and M. Y. Vardi. Benefits of bounded model checking in an industrial setting. LNCS, 2101:436-453, 2001.    [9] Satyaki Das and David L. Dill. Successive approximation of abstract transition relations. In Symposium on Logic in Computer Science, pages 51-60. IEEE, 2001.    [10] J.-C. Filliâtre, S. Owre, H. Rueβ, and N. Shankar. ICS: Integrated Canonizer and Solver. LNCS, 2102:246-249, 2001.    [11] Rob Gerth, Doron Peled, Moshe Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification Testing and Verification, pages 3-18, Warsaw, Poland, 1995. Chapman & Hall.    [12] A. Goel, K. Sajid, H. Zhou, and A. Aziz. BDD based procedures for a theory of equality with uninterpreted functions. LNCS, 1427:244-255, 1998.    [13] T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193-244, June 1994.    [14] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre. Lazy abstraction. ACM SIGPLAN Notices, 31(1):58-70, 2002.    [15] Orna Kupferman and Moshe Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291-314, 2001.    [16] Yassine Lachnech, Saddek Bensalem, Sergey Berezin, and Sam Owre. Incremental verification by abstraction. LNCS, 2031:98-112, 2001.    [17] M. O. Möller, H. Rueβ, and M. Sorea. Predicate abstraction for dense real-time systems. Electronic Notes in Theoretical Computer Science, 65(6), 2002.    [18] O. Möller and H. Rueβ. Solving bit-vector equations. LNCS, 1522:36-48, 1998.    [19] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC'01), June 2001.    [20] G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1 (2):245-257, 1979.    [21] S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748-752. Springer-Verlag, 1992.    [22] David A. Plaisted and Steven Greenbaum. A structure preserving clause form translation. Journal of Symbolic Computation, 2(3):293-304, September 1986.    [23] A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domains instantiations. LNCS, 1633:455-469, 1999.    [24] H. Rueβ and N. Shankar. Deconstructing Shostak. In 16th Symposium on Logic in Computer Science (LICS 2001). IEEE Press, June 2001.    [25] Vlad Rusu and Eli Singerman. On proving safety properties by integrating static analysis, theorem proving and abstraction. LNCS, 1579:178-192, 1999.    [26] H. Saïdi. Modular and incremental analysis of concurrent software systems. In 14th IEEE International Conference on Automated Software Engineering, pages 92-101. IEEE Computer Society Press, 1999.    [27] Robert Shostak. Deciding linear inequalities by computing loop residues. Journal of the ACM, 28(4):769-779, October 1981.    [28] A. P. Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6(5):495-512, 1994.
Model checking decides the problem of whether a system satisfies a temporal logic property by exploring the underlying state space. It applies primarily to finite-state systems but also to certain infinite-state systems, and the state space can be represented in symbolic or explicit form. Symbolic model checking has traditionally employed a Boolean representation of state sets using binary decision diagrams (BDD) [4] as a way of checking temporal properties, whereas explicit-state model checkers enumerate the set of reachable states of the system.
Recently, the use of Boolean satisfiability (SAT) solvers for linear-time temporal logic (LTL) properties has been explored through a technique known as bounded model checking (BMC) [7]. As with symbolic model checking, the state is encoded in terms of booleans. The program is unrolled a bounded number of steps for some bound k, and an LTL property is checked for counterexamples over computations of length k. For example, to check whether a program with initial state I and next-state relation T violates the invariant Inv in the first k steps, one checks, using a SAT solver:I(s0)T(s0, s1) . . . T(sk-1, sk)(Inv(s0) . . . Inv(sk))
This formula is satisfiable if and only if there exists a path of length at most k from the initial state s0, which violates the invariant Inv. For finite state systems, BMC can be seen as a complete procedure since the size of counterexamples is essentially bounded by the diameter of the system [3]. It has been demonstrated that BMC can be more effective in falsifying hypotheses than traditional model checking [7, 8].
It is possible to extend the range of BMC to infinite-state systems by encoding the search for a counterexample as a satisfiability problem for the logic of Boolean constraint formulas. For example, the BMC problem for timed automata can be captured in terms of a Boolean formula with linear arithmetic constraints. But the method presented here scales well beyond such simple arithmetic clauses, since the main requirement on any given constraint theory is the decidability of the satisfiability problem on conjunctions of atomic constraints. Possible constraint theories include, for example, linear arithmetic, bitvectors, arrays, regular expressions, equalities over terms with uninterpreted function symbols, and combinations thereof [20, 24].
Whereas BMC over finite-state systems deals with finding satisfying Boolean assignments, its generalization to infinite-state systems is concerned with satisfiability of Boolean constraint formulas. There has been much recent work in reducing the satisfiability problem of Boolean formulas over the theory of equality with uninterpreted function symbols to a SAT problem [5, 12, 23] using eager encodings of possible instances of equality axioms. Barrett, Dill, and Stump [2] describe an integration of Chaff with CVC by abstracting the Boolean constraint formula to a propositional approximation, then incrementally refining the approximation based on diagnosing conflicts using theorem proving, and finally adding the appropriate conflict clause to the propositional approximation. This integration corresponds directly to an online integration in the lazy theorem proving paradigm. Their approach to generate good explanations is to extend CVC with a capability of abstract proofs for overapproximating minimal sets of inconsistencies. Also, optimizations based on don't cares are not considered in [2].
Initial experiments with PVS [21] strategies, based on a combination of BDDs for propositional reasoning and a variant of loop residue [27] for arithmetic, it was only possible to construct counterexamples of small depths (≦5). More specialized verification techniques are needed. Because BMC problems are often propositionally intensive, it seems to be more effective to augment SAT solvers with theorem proving capabilities, such as ICS [10], than add propositional search capabilities to theorem provers.